| Model: | philosophers v.1 (CTMC) |
| Parameter(s) | N = 20, TIME_BOUND = 1 |
| Property: | MaxPrReachDeadlockTB (prob-reach-time-bounded) |
java -Xms10240m -Xmx10240m -jar ./root/epmc-standard.jar check --model-input-files philosophers.20.jani --model-input-type jani --property-input-names MaxPrReachDeadlockTB --translate-messages false --value-floating-point-output-native true --graphsolver-iterative-stop-criterion relative --graphsolver-iterative-tolerance 1e-6 --const TIME_BOUND=1
| Walltime: | 1.8116564750671387s |
| Return code: | 0 |
| Note(s): | The tool result '0' is tagged as incorrect. The reference result is 'OrderedDict([('lower', 6.320794925e-06), ('upper', 6.320994925e-06)])' (approx. OrderedDict([('lower', 6.320794925e-06), ('upper', 6.320994925e-06)])) which means a relative error of '1.0' which is larger than the goal precision '0.001'. |
| Relative Error: | 1.0 |
assertions-disabled model-checking analysing-property MaxPrReachDeadlockTB start-building-explorer start-building-initial-states-explorer done-building-initial-states-explorer done-building-explorer build-model-start build-model-done 1 0 num-states-in-filter 1 "initial" printing-all-filter-results print-filter 0 0 0.0 model-checking-done 0 command-check-result-is 0.0 MaxPrReachDeadlockTB